package tr.edu.ege.kipler.satisfiability.container;

import java.util.HashSet;
import java.util.Set;

import tr.edu.ege.kipler.common.Copyable;
import tr.edu.ege.kipler.satisfiability.UnsatisfiableException;
import tr.edu.ege.kipler.satisfiability.syntactical.FormulaSimplificationVisitor;
import tr.edu.ege.kipler.satisfiability.syntactical.TopConsistenceNormalFormVisitor;
import tr.edu.ege.kipler.syntax.WorldElement;
import tr.edu.ege.kipler.syntax.atomicformula.ConceptDefinition;

/**
 * 
 * @author İnanç Seylan
 *
 */
public class GeneralTBox implements Copyable<GeneralTBox>, FormulaBase {
	private Set<ConceptDefinition> positiveFormulas = new HashSet<ConceptDefinition>();

	private Set<ConceptDefinition> negatedFormulas = new HashSet<ConceptDefinition>();

	public boolean isSatisfiable() {
		return true;
	}

	private WorldElement generateNormalForm(WorldElement formula) {
		formula = formula.copy();
		TopConsistenceNormalFormVisitor topVisitor = new TopConsistenceNormalFormVisitor();
		formula.accept(topVisitor);
		formula = topVisitor.getNormalForm();
		FormulaSimplificationVisitor simpleVisitor = new FormulaSimplificationVisitor();
		formula.accept(simpleVisitor);
		formula = simpleVisitor.getNormalForm();
		return formula;
	}

	private Set<ConceptDefinition> decideOnSet(ConceptDefinition cd) {
		return cd.isNegated() ? negatedFormulas : positiveFormulas;
	}

	public void add(WorldElement formula) throws UnsatisfiableException {
		if (formula instanceof ConceptDefinition) {
			add((ConceptDefinition) formula);
		}
	}

	public void add(ConceptDefinition conDef) {
		ConceptDefinition normalized = (ConceptDefinition) generateNormalForm(conDef);
		decideOnSet(normalized).add(normalized);
	}

	public Set<ConceptDefinition> getPositiveGCDs() {
		return positiveFormulas;
	}

	public Set<ConceptDefinition> getNegatedGCDs() {
		return negatedFormulas;
	}

	public Set<WorldElement> getFormulas() {
		Set<WorldElement> result = new HashSet<WorldElement>(positiveFormulas);
		result.addAll(negatedFormulas);
		return result;
	}

	public GeneralTBox copy() {
		GeneralTBox tbox = new GeneralTBox();
		tbox.positiveFormulas = new HashSet<ConceptDefinition>(positiveFormulas);
		tbox.negatedFormulas = new HashSet<ConceptDefinition>(negatedFormulas);
		return tbox;
	}

	public boolean contains(WorldElement f) {
		boolean result = false;
		if (f instanceof ConceptDefinition) {
			result = contains((ConceptDefinition) f);
		}
		return result;
	}

	public boolean contains(ConceptDefinition cd) {
		return decideOnSet(cd).contains(cd);
	}

	@Override
	public boolean equals(Object obj) {
		if (obj != null && (obj.getClass().equals(this.getClass()))) {
			GeneralTBox other = (GeneralTBox) obj;
			return positiveFormulas.equals(other.positiveFormulas)
					&& negatedFormulas.equals(other.negatedFormulas);
		}
		return false;
	}

	@Override
	public String toString() {
		StringBuffer buffer = new StringBuffer();
		for (WorldElement f : getFormulas())
			buffer.append(f + ", ");
		buffer.delete(buffer.length() - 2, buffer.length());
		return buffer.toString();
	}

}
